\begin{dis}{\LARGE\scshape Diccionario}
\especif
\\\hspace*{2em}Se usara el TAD Dicc($\alpha$, $\beta$) dado por la catedra

\aspectos
\serviciosexp
\\ \hspace*{2em} Todas las operaciones se realizan por referencia\\
\orden{}{}
\orden{}{}
\orden{}{}
\orden{}{}
\orden{}{}
\orden{}{}
\orden{}{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\interfaz
\interface{Dicc(\alpha,\beta)}

\seexplica{Dicc(\alpha,\beta)}
\usa{\scshape Bool, Nat, \alpha, \beta, Conj, Cola \normalfont} 
\exporta{Dicc, definir, definido, obtener, borrar, claves, =$_{dicc}$}
\genero{Dicc(\alpha, \beta)}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\operaciones

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{Dicc}{}{res: Dicc($\alpha$,$\beta$)}{}
   \precond{True}
   \poscond{\widehat{res} \igobs vacio}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{definir}{in a: $\alpha$, in b: $\beta$, inout d: Dicc($\alpha$,$\beta$)}{}
   \precond{True}
   \poscond{widehat{d} $\igobs$ definir(\widehat{a},$d_0$}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{3em} \begin{funcion}{definido}{in a: $\alpha$, in d: Dicc($\alpha$,$\beta$)}{res: bool}{}
   \precond{True}
   \poscond{\widehat{res} $\igobs$ def?(\widehat{a}, \widehat{c})}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{obtener}{in a: $\alpha$,  in d: Dicc($\alpha$,$\beta$)}{res: bool}
   \precond{def?(\widehat{a},\widehat{d})}
   \poscond{\widehat{res} $\igobs$ obtener(\widehat{a},\widehat{d})}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{borrar}{in a: $\alpha$, inout d: Dicc($\alpha$,$\beta$)}{}{}
   \precond{def?(\widehat{a},\widehat{d})}
   \poscond{widehat{d} $\igobs$ borrar(\widehat{a},$d_0$)}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{claves}{in d: Dicc($\alpha$,$\beta$)}{res: conj($\alpha$)}{}
   \precond{True}
   \poscond{widehat{res} $\igobs$ claves($d_0$)}
\end{funcion}

\hspace*{1em} \textcolor{red}{--------------------------------------------------------------------} \\
\hspace*{1em} \begin{funcion}{=$_{Dicc}$}{in d: Dicc($\alpha$,$\beta$), in p: Dicc($\alpha$,$\beta$)}{res: bool}{}
   \precond{True}
   \poscond{\widehat{res} \igobs c \igsub{dicc} p} 
\end{funcion}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\pautas

\estructura \\ \normalfont
\\\hspace*{2em}Para cumplir los requerimientos pedidos, vamos a usar un arreglo Dimensionable con una
\\\hspace*{2em}secuencia en cada bucket y una funcion de hash para acomodar los elementos.

\\\hspace*{2em}Dicc se representa con \textbf{estrDicc}
\\\hspace*{2em}donde \textbf{estrDicc} es Tupla $<$ arD : arreglo$\_$dimensionable de Cola($\beta$), clavD : Conj($\alpha$)$>$ \\

\invariante\\
\\\hspace*{2em}Rep: \widehat{estrDicc} $\longrightarrow$ boolean \\
\\\hspace*{2em}($\forall$ e: estrDic) Rep(e) $\equiv$ ($\forall$ a: $\alpha$ $\in$ e.clavD)\\
\\\hspace*{2em} (
\funcabs \\
\\\hspace*{2em}Abs: \widehat{estrDicc} e $\longrightarrow$ Dicc \\\hspace*{4em}Res(e)\\
\\\hspace*{2em}($\forall$ e: \widehat{estrDicc}) Abs(e) $\equiv$ d: Dicc \\
\\\hspace*{2em}($\forall$ a: $\alpha$)
\\\hspace*{2em} def?(a, d) \igobs definido(a, e) \\
\\\hspace*{2em} obtener(a, d) \igobs obtener(a, e) \\
\textbf{Funciones auxiliares:} \\ 
\\\hspace*{1em} cantRep : bloque $x$ arreglo$\_$dimensionable $x$ Nat $\longrightarrow$ Nat  
\\\hspace*{1em} cantRep(b, a, n) $\equiv$ if n = 0 then 0 else if esta?(b, a[n]) then 1 + cantRep(s, a, n-1)

\end{dis}